\begin{tabbing}
$M$.rframe($A$.sends ${\it tfL}$ of $k$ on $l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$$\in$dom(($M$.2.2.2.2.2.2.2.2.2.2).1). \+
\\[0ex]
\\[0ex]$L$\==($M$.2.2.2.2.2.2.2.2.2.2).1($x$) $\Rightarrow$ \+
\\[0ex]($\uparrow$deq{-}member(KindDeq;$k$;$L$))
\-\\[0ex]$\vee$ \=($\forall$$s_{1}$, $s_{2}$:$A$.state, $v$:$A$.da($k$).\+
\\[0ex]($s_{1}$ $\equiv$ $s_{2}$ mod $x$) $\Rightarrow$ ($\forall$$i$:\{0..$\parallel$${\it tfL}$$\parallel^{-}$\}. (${\it tfL}$[$i$].2)($s_{1}$,$v$) = (${\it tfL}$[$i$].2)($s_{2}$,$v$)))
\-\-
\end{tabbing}